Step of Proof: nat_ind 12,41
Inference at * 1 0 1 2 1 1 
Iof proof for Lemma nat ind:

.....basecase..... NILNIL

1. P : {k}
2. P(0)
3. i:. P(i - 1)  P(i)
  P(0) 
latex
 by Id  
latex

 1: .....basecase..... NILNIL

 1:   P(0)
 .

origin